COMMENT ⊗   VALID 00018 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.require "memo.pub[let,jmc]" source
C00004 00003	Abstract: An Elephant program is a collection of sentences of first order
C00007 00004	#. %3Introduction%1
C00012 00005	#. %3Expressing a sequential program in Elephant%1
C00021 00006	#. %3Reversing a list%1
C00026 00007	#. %3Another Elephant Formalism%1
C00032 00008	.if true then begin "defining functions"
C00033 00009	#. Non Immediate Elephant Programs
C00035 00010	#. An airline reservation system
C00039 00011	.if false then begin
C00043 00012	#. %2samefringe%1
C00047 00013	#. Parallel processes for computing a sum of functions
C00052 00014	#. Equivalence of Elephant programs.
C00058 00015	#. Remarks
C00065 00016	#. References
C00068 00017	.if false then begin
C00072 00018	.end
C00076 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.every heading (,incomplete draft,{page});
.at "qg" ⊂"%3go_to%*"⊃
.at "qNIL" ⊂"%1NIL%*"⊃
.at "qt" ⊂"%At%*"⊃
.at "qF" ⊂"%AF%*"⊃
.turn on "→"
.group skip 15
.cb THE ELEPHANT LANGUAGE FOR PROVING AND MAYBE EVEN PROGRAMMING
.skip 1
.once center
by John McCarthy


.item←0
Abstract: An Elephant program is a collection of sentences of first order
logic.  Corresponding to each program variable (say ⊗x) in an Algol-type
program, there is a function (say ⊗x(t)) of time in the Elephant program.
Each sentence tells how the value of ⊗x(t) depends on the values of the
variables at earlier times.  The %2program counter%1 is treated as just
another variable.

	The sentence representing a combination of flowcharts is
just the conjunction of the sentences representing the flowcharts
separately.  Properties of Elephant programs are expressed as first order
sentences in the language of the data domain augmented by the names of
the functions constituting the program.  The usual methods for proving
properties of programs require no new formalism; they are just styles of
proof in first order logic.

	Besides representing ordinary sequential and parallel programs,
Elephant can represent programs that refer to the past of variables and
therefore avoid explicit mention of many data structures.
Since we often refer to the past in expressing processes in natural
language, a computer language that doesn't allow it cannot claim
to be "natural".
.skip to column 1
#. %3Introduction%1
.double space

	The Elephant algorithmic language
represents program variables as functions of a time variable %2t%1.
Instead of a variable ⊗x as in an Algol program, an Elephant program
would have a function
⊗x(t), and instead of an assignment statement %2x_:=_...%1, we may use an
equation %2x(t+1)_=_...%1 or sometimes %2x(t)_=_...%1.  The Elephant
formalism has two uses.

	First, Elephant provides a simple way of expressing sequential
programs as sentences in a first order theory which can then be used to
prove properties of the program.  Elephant is dual to the first order
representation of recursive programs described in (Cartwright 1976) and
(Cartwright and McCarthy 1979) in that an Elephant program describes
what is to happen at successive times starting with the initial state,
while a recursive description describes how a desired function is
computed with the help its values for
simpler sets of arguments.  Another analogy is to say
that Elephant is bottom-up while recursive programs are
top-down.

	Once a program has been expressed in Elephant, the %2inductive
assertion%1 and %2intermittent assertion%1 methods are automatically
available as particular techniques of making proofs within first order
logic.  They amount to using particular kinds of lemmas in proving
theorems.  Instances of the Hoare axioms are also just lemmas.

	The second aspect of Elephant (the original
motivation) is the ability to refer to the
whole past of the variables without specifying data structures for
remembering what has to be known in order to perform a current action.
Thus a reservation program written in Elephant can say that a passenger
has a reservation if he has made one and not cancelled it.  The program
needn't specify any data structure for remembering who has reservations;
%2an elephant never forgets%1.  Likewise, the rule that a castling
move is prohibited if the rook or king involved has ever moved is directly
expressible without inventing a variable to hold the information.

	Such reference to the past is certainly used in informal
English descriptions of what we want a computer to do.  Therefore, a
sufficiently high level programming language must have it.  On the other
hand, the Elephant programs that I have been able to write that refer
to the past are often more difficult to write and read than programs
with explicit data structures.  Perhaps I am simply inexperienced in
writing Elephant program, perhaps extensions to the formalism are
needed, and perhaps an approach different from Elephant will work better
in referring to the past.

	The simplest way to begin is with examples.

.skip 3
#. %3Expressing a sequential program in Elephant%1
.a←item

	Consider the following Algol 60 program fragment (declarations
omitted) for doing multiplication by iterated addition:

.begin nofill
%2

start:	i := n;				∂(30)0
	p := 0;				∂(30)1
loop:	qif i = 0 qthen qg done;	∂(30)2
	i := i - 1;			∂(30)3
	p := p + m;			∂(30)4
	qg loop;			∂(30)5
.end

One corresponding Elephant program consists of the sentences

.begin nofill
.zz←12
%2

pc(0) =start,

∀t.[i(t+1) →=_∂(zz)IF pc(t) = start THEN n
∂(zz)ELSE IF pc(t) = start + 3 THEN i(t) - 1
∂(zz)ELSE IF start ≤ pc(t) ≤ start + 5 THEN i(t)
∂(zz)ELSE i(t+1)],

∀t.[p(t+1) →=_∂(zz)IF pc(t) = start + 1 THEN 0
∂(zz) ELSE IF pc(t) = start + 4 THEN p(t) + m
∂(zz)ELSE IF start ≤ pc(t) ≤ start + 5 THEN p(t)
∂(zz)ELSE p(t+1)],

%1and%2

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = start + 2 ∧ i(t) = 0 THEN done
∂(zz)ELSE IF pc(t) = start + 5 THEN start + 2
∂(zz)ELSE IF start ≤ pc(t) ≤ start + 5 THEN pc(t+1)
∂(zz)ELSE pc(t+1].
.end

	In these equations ⊗i(t) and ⊗p(t) replace the simple
variables of the Algol program.  The function ⊗pc(t) is the
program counter, and it takes values from %2start+1%1 to %2start+5%1.
Notice the numbers written on the right of the Algol program.  It is
be apparent from the example that any program made up of assignments
and qgs can be systematically translated to an Elephant program.
We have used the logical conditional expression %2IF_..._THEN_..._ELSE%1
rather than qif_..._qthen_..._qelse, because there is no reason to
provide for an undefined case.  (The distinction is discussed in
(McCarthy and Talcott 1979)).
.if false then begin
If the reader is a reactionary and
refuses to admit conditional expressions as terms in first order
logic, then they can be eliminated.  The equation for ⊗i(t+1) would
then split into the three cases

.begin nofill
%2

∀t.[pc(t) = 0 ⊃ i(t+1) = 0 ∧ pc(t) = 1 ⊃ i(t+1) = i(t) - 1
∂9∧ pc(t) ≠ 0 ∧ pc(t) ≠ 1 ⊃ i(t+1) = i(t)]
.end
.end

	Notice also that the length of the Elephant program is linear in the
length of the Algol program.

	Having one value of ⊗pc(t) for
each statement in the Algol program is unnecessary, although it makes
the systematic character of the translation more apparent.  If we
let %2pc(t)_=_start%1 correspond to the initialization and %2pc(t)_=_start+1%1
correspond to the loop, then the equations become

.begin nofill
.zz←12
%2

pc(0) = 0,

∀t.[i(t+1) →=_∂(zz)IF pc(t) = start THEN n
∂(zz)ELSE IF pc(t) = start+1 ∧ i(t) ≠ 0 THEN i(t) - 1
∂(zz)ELSE IF start ≤ pc(t) ≤ start+1 THEN i(t)
∂(zz)ELSE i(t+1)],

∀t.[p(t+1) →=_∂(zz)IF pc(t) = start THEN 0
∂(zz) ELSE IF pc(t) = start+1 ∧ i(t) ≠ 0 THEN p(t) + m
∂(zz)ELSE IF start ≤ pc(t) ≤ start+1 THEN p(t)
∂(zz)ELSE p(t+1)],

%1and%2

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = start+1 THEN (IF i(t) = 0 THEN done ELSE start+1)
∂(zz)ELSE IF start ≤ pc(t) ≤ start+1 THEN pc(t) + 1
∂(zz)ELSE pc(t+1)].
.end

	That these programs compute the product of ⊗m and ⊗n is specified
by the sentence

	%2∃t.[pc(t) = done ∧ p(t) = m*n]%1.

It is provable from any first order axiomatization of arithmetic
together with the sentences constituting the program.  No special
axioms for programs or "logic of programs" is required.
One need only apply mathematical induction to the predicate

	%2qF(j) ≡ ∃t.(pc(t) = start+2 ∧ p(t) = m(n - i(t)) ∧ i(t) = j
⊃ ∃t.(pc(t) = done ∧ p(t) = mn)%1

The case %2j = 0%1 follows from the equation for ⊗pc(t+1), and the
induction step also follows from the Elephant program.  The desired
result is the conclusion of %2qF(n)%1, and the premiss
of %2qF(n)%1 follows from the initial conditions.

	Thus an entirely conventional mathematical way of writing
recursion equations leads to a convenient programming language.  It
is tempting to call the language Algol 50, since it only uses ideas that
were familiar in 1950.

	The proof of correctness for this
multiplication program is misleadingly simple, since
we can easily write explicit formulas for ⊗i(t), ⊗p(t), and
⊗pc(t) and prove them by mathematical induction.  More typical proofs
occur when it isn't convenient to give explicit formulas for the
variables as functions of time or for the value of ⊗t for which the
program terminates.  Then the computational content of the proof is
is often essentially the same as that of an %2inductive assertions%1 proof
combined with induction on a rank function of the variables taking
values in a suitable inductively ordered set.

.skip 3
#. %3Reversing a list%1

	Reversing a list provides another example of an Elephant program
that can be compared with a recursive conditional expression program
for the same function.  We start with a Lisp "program feature" program
written in the style of Algol 60.
.begin nofill
%2
.z←8

∂zu := w;
∂zv := qNIL;
∂1loop:	∂zqif null u qthen qg done;
∂zv := [qa u] . v;
∂zu := qd u;
∂zqg loop;
∂1done:

.end

	The corresponding Elephant program is

.begin nofill
%2
.zz←12

pc(0) = 0,

∀t.[u(t+1) →=_∂(zz)IF pc(t) = 0 THEN w
		∂(zz)ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN qd u(t)
		∂(zz)ELSE u(t)],

∀t.[v(t+1) →=_∂(zz)IF pc(t) = 0 THEN qNIL
		∂(zz) ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN qa u(t) . v(t)
		∂(zz) ELSE v(t)]

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = 1 ∧ ¬null u(t) THEN 1
		∂(zz)ELSE pc(t) + 1].
.end

	This can be compared with the LISP program ⊗reverse defined by

	%2reverse u ← qif qn u qthen qNIL qelse reverse qd u * <qa u>%1.

With the latter, as shown in (Cartwright and McCarthy 1979), it is
convenient to prove such properties as %2reverse_reverse_u_=_u%1 and
%2reverse[u_*_v]_=_reverse_v_*_reverse_u%1.  The major fact about
the Elephant program is expressed by

	%2∃t.(pc(t) = 2 ∧ v(t) = reverse w)%1.

It can be proved by proving that %2length u(t)%1 is a decreasing function
of ⊗t, i.e. for any ⊗t such that ⊗pc(t)_<_2, there is %2t'_>_t%1 such
that %2length_u(t')_<_length_t%1, and also that

	%2∀t.[reverse_w = reverse u(t) * v(t)]%1.

This is just another %2inductive assertions%1 proof.  So far it seems that
the most convenient technique for proving facts about Elephant programs
is %2inductive assertions%1,
which is less flexible than the technique described in (Cartwright and
McCarthy 1979) that uses the %2functional equation%1 and the %2minimization
schema%1.  This is because %2inductive assertions%1 provides no way
of expressing algebraic relations among functions defined by programs.

	One mathematically straightforward way of defining functions by
programs is the following.  We rewrite the above equations to introduce
⊗w as an explicit argument of the functions so that they become ⊗u(t,w), 
⊗v(t,w), and pc(t,w).  We then define a relation ⊗reverses(v,w) by

	%2∀v w.(reverses(v,w) ≡ ∃t.(pc(t,w) = 2 ∧ v(t,w) = v))%1.

When we have proved %2∀w ∃!v.reverses(v,w)%1, first order logic
entitles us to replace the relation ⊗reverses by a function.  We can
then prove successively that this function satisfies the relations

	%2reverse qNIL = qNIL%1,

	%2reverse [x . u] = reverse u * <x>%1

	%2reverse reverse u = u%1,

and

	%2reverse[u * v] = reverse v * reverese u%1,

where the notation is as in (McCarthy and Talcott 1979).

.skip 3
#. %3Another Elephant Formalism%1

	The Elephant formalism of the previous sections sorts the program
by variables, while a sequential program sorts it according to the program
counter.  The latter is more conventional and often more convenient.
Moreover, if we want to represent pieces of program separately and
combine them by taking conjunctions, sorting by program counter seems
to work better.

	Our pc-sorted Elephant involves three changes:

	1. Instead of writing ⊗x(t), we write ⊗value(x,t).  This allows
us to quantify over variables and is useful for combining the qelse
cases.

	2. Instead of starting the program counter at 0, we give each
program a symbolic entry location.  This is analogous to the machine
language idea of a relocatable program, and it has the same use.
It enables us to combine programs by conjunction, and we can suppose
that numerical values of the entry locations of the parts of the
program are specified so that no distinct parts of the programs have
the same values of the program counter.  Indeed
specifying the values of the entry locations in a way that corresponds
to overlapping programs will usually lead to a contradiction in
the combined sentence.

	3. We have one equation that specifies ⊗value(var,t+1)).  Its right
side is a conditional expression whose clauses correspond to the
different values of the program counter.

	With all these changes, our program ⊗P1 for multiplication by
addition is

.begin nofill
.zz←12

%2
∀var t.[value(var,t+1) =
∂(zz)IF value(pc,t) = entry1 ∧ var = i THEN n
∂(zz)ELSE IF value(pc,t) = entry1 + 1 ∧ var = p THEN 0
∂(zz)ELSE IF value(pc,t) = entry1 + 2 ∧ var = pc ∧ value(i,t) = 0 THEN exit1
∂(zz)ELSE IF value(pc,t) = entry1 + 3 ∧ var = i THEN value(i,t) - 1
∂(zz)ELSE IF value(pc,t) = entry1 + 4 ∧ var = p THEN value(p,t) + 1
∂(zz)ELSE IF value(pc,t) = entry1 + 5 ∧ var = pc THEN entry1 + 2

∂(zz)ELSE IF entry1 ≤ value(pc,t) ≤ entry1 + 5 ∧ var = pc THEN value(pc,t) + 1
∂(zz)ELSE IF entry1 ≤ value(pc,t) ≤ entry1 + 5 THEN value(var,t)
∂(zz)ELSE value(var,t+1)%1

.end

	Notice that there is one clause for each statement in the Algol
program and three additional clauses.  The first additional clause states that
the program counter is increased by 1 within the program unless something
else is previously stated about that value
of the program counter.  The second states that variables
whose behavior is not previously specified in the program retain their
values within the program segment.  The last clause manages, by being
tautologous, to say nothing about what happens outside of the range
%2entry1_≤_pc_≤_entry1+5%1, thus avoiding interference with sentences
specifiying other programs that might be combined with ⊗P1. 

	Indeed suppose ⊗P2 is another program involving some of the same
same variables as ⊗P1 and possibly some others, and suppose we
want to combine these programs so that ⊗P2 is executed after ⊗P1.
We need only take the conjunction of the sentences together with
the sentence %2entry2_=_exit1%1.  Should we want to do so, we
can transform the conjunction into an equivalent sentence which
has the same form as ⊗P1 or ⊗P2, i.e. a clause for each statement
and three clauses at the end.

	The method of combination by conjunction works the same
in more complicated cases.  A program can have multiple entries
and exits, any exit can be connected to any entry just by equating
suitable ⊗entry and ⊗exit parameters.
.if true then begin "defining functions"

#. Defining Functions in Elephant

	Given a relation ⊗P(x,y), we can partially define a function ⊗f by

	%2∀x.(∃y.P(x,y) ⊃ P(x,f(x)))%1

provided ⊗f is a fresh function symbol.  If we
can prove ⊗∀x∃!y.P(x,y), then we will be able to prove that ⊗f is
total.  In the Elephant context we can write

	%2∀x.(∃t.(pc(t,x) = done ∧ ∀t'(t' < t ⊃ pc(t')≠done))
⊃ pc(qt(x),x) = done ∧ ∀t'.(t' < qt(x) ⊃ pc(t') ≠ done))%1

defining a function qt and writing

	%2∀x.(f(x) = y(qt(x),x))%1.

.end "defining functions"
#. Non Immediate Elephant Programs

	When we translate an Algol program into Elephant, we get
equations in which the %2x(t+1)%1s depend only on the %2x(t)%1s.
We will call such a program an %2immediate%1 Elephant program.
However, the recursion
equations will still have guaranteed solutions if the %2x(t)%1s depend on
arbitrary earlier values of ⊗t.  This leads to a "high level" programming
language with the following features:

	1. The program refers to the past through earlier values of
⊗t, just as though everything were remembered.  That's why we call
the language Elephant, since an Elephant never forgets.

	2. The compiler is smart and decides what data structures are
required in order to carry out the computations without remembering
everything.  To the extent that compilers can be written that do this
effectively, Elephant is a "higher level" language in which the
programer specifies less than in Algol, etc.

#. An airline reservation system

	Consider programming a trivial airline reservation system.
We want to say that %2a passenger has a reservation if he
has made one that has not been cancelled%1.  We do not want to prescribe
what data structures have to be kept in order to be able to answer the
question of whether someone has a reservation.

	This program replies properly to requests to make reservations,
cancel them, and to inquiries about whether a reservation exists.
The program refers to its input in
terms of an abstract analytic syntax the meaning of whose mnemonic
predicate and function names is hopefully obvious.  The only data
structure explicitly mentioned is the number of seats currently occupied,
and even that could be eliminated from the program.  The Elephant compiler,
therefore, gets the honor of determining what other data structures
are needed.  We use the convention of writing %2α{xα}f%1 instead of ⊗f(x) when
it is convenient to write the argument before the function name.
.begin nofill
.uu←35
%2

∀t.[output(t+1) = α{input(t)α}[λ in.
∂(10)IF ismake in THEN →[∂(uu)IF hasrev(maker in,t) THEN "You had it"
			∂(uu)ELSE IF number(t) = N THEN "No room"
			∂(uu)ELSE "You have it now"]
∂(10)ELSE IF iscancel in THEN →[∂(uu)IF hasrev(maker in,t) THEN "It's cancelled"
			∂(uu)ELSE "You don't have it to cancel"]
∂(10)ELSE IF isinquiry in THEN→[∂(uu)IF hasrev(maker in,t) THEN "You have one"
			∂(uu)ELSE "You don't have one"]
∂(10)ELSE qNIL]

∀t.[number(t+1) = α{input(t)α}[λ in.
∂(10)IF ismake in THEN →[∂(uu)IF hasrev(maker in,t) ∨ number(t) = N
∂(uu)THEN number(t)
∂(uu)ELSE number(t) + 1]
∂(10)ELSE IF iscancel in THEN →[∂(uu)IF hasrev(maker in,t) THEN number(t) - 1
			∂(uu)ELSE number(t)]
∂(10)ELSE number(t)]
.end

where

	%2∀t.[hasrev(passenger,t) ≡ ∃t1.(t1 < t ∧ ismake input t1 ∧
passenger = maker input t1 ∧ number(t1) < N) ∧ ¬∃t2.(t1 < t2 < t ∧
iscancel input t2 ∧ maker input t2 = passenger))]%1.

	The main difficulty in making a compiler for Elephant is illustrated
by the predicate ⊗hasrev.  The compiler has to understand that it
must remember successful reservations but can forget unsuccessful
attempts at making a reservation and that it can forget reservations
that have been cancelled.  Perhaps ⊗hasrev should be written using primitives
that refer explicitly to the most recent occurrence of an event,
which might permit a less intelligent compiler.

.if false then begin
#. Elephant program to count vertices in a list structure

.begin nofill
****
There seems to be a bug in this program and the %2samefringe%1 program
that we hope to fix in a subsequent draft.
****
.end

	Another context in which it is possible to avoid specifying a
data structure by referring to the past, occurs when a list structure
is to be scanned.  The simplest example is a program to count the
vertices in a list structure.

Here ⊗a is the list structure being scanned, ⊗x is a running variable for
the current structure, and ⊗n is the current count.

	Because of Elephant's ability to refer to the past, we can
write this program without specifying a stack.  It is up to the compiler
to decide that a stack is appropriate for implementing the algorithm.

.begin nofill
%2 

∀t.[x(t+1) →=_∂(16)IF pc(t) =_0 THEN a
∂(16)ELSE IF pc(t) =_1 THEN
→[∂(22)IF [∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(30)THEN x(t)
∂(22)ELSE IF ¬atom x(t) ∧ ¬seen(car x(t),t) then car x(t)
∂(22)ELSE cdr x(mostrecent(t,λt1.¬seen(cdr(x(t1)),t)))]
∂(16)ELSE x(t)]

∀t.[n(t+1) →=_∂(16)IF pc(t) =_0 THEN 0
∂(16)ELSE IF ∂(25)pc(t) =_1 
→∧ ∂(25)¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(30)THEN n(t) + 1
∂(16)ELSE n(t)]

∀t.[pc(t+1) →=_∂(16)IF ∂(20)pc(t) =_1
→∧ ∂(20)¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(25)THEN 1
∂(16)ELSE pc(t) + 1
.end

where the predicate ⊗seen and the functional ⊗mostrecent are defined as
follows:
.begin nofill
%2 

∀y t.[seen(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x(t1)]]

∀t.[mostrecent(t, pred) = qif pred t qthen t qelse mostrecent(t - 1, pred)].
.end

We would like to regard these as definitions not as programs.  Indeed the
compiled program shouldn't compile them directly, but should do the job
another way that uses time and space more efficiently.

Of course, this example is less perspicuous than the Lisp program

%2count x ← qif qat x qthen 1 qelse count qa x + count qd x%1

which scans the vertices in the same order.  But then this problem
is especially appropriate for recursion and Lisp's built-in stack
mechanism.

Most likely ⊗seen and ⊗mostrecent will occur in other algorithms
where one doesn't want to look at things that have been already tried.

#. %2samefringe%1

	The LISP predicate %2samefringe[x,y]%1 may be defined by

%2samefringe[x1,x2] ≡ fringe x1 = fringe x2%1,

where %2fringe_x%1 is a list of the atoms in ⊗x and is defined by

%2fringe x ← qif qat x qthen <x> qelse fringe qa x . fringe qd x%1.

	The above definition does not provide the most efficient
computation of ⊗samefringe, and a better LISP function is given
in (Cartwright and McCarthy 1979), and a proof of its correctness
is outlined.  A detailed computer-checked proof is given in
(Talcott 1979).

	The following is an Elephant program for %2samefringe%1.

.begin nofill
%2
.a←12;b←28;c←35;

pc(0) = 0

∀t.[x1(t+1) →=_∂aIF pc(t) = 0 THEN x1
∂aELSE IF pc(t) = 1 THEN
→[∂bIF [∃y.seen1(y,t) ∧ ¬atom y ∧ [¬seen1(car y,t) ∨ ¬seen1(cdr y,t)]
∂cTHEN cdr x1(mostrecent(t,λt1.¬seen1(cdr(x1(t1)),t)))
∂bELSE x1(t)]
∂aELSE IF pc(t) = 2 THEN
→[∂bIF [∃y.seen1(y,t) ∧ ¬atom y ∧ [¬seen1(car y,t) ∨ ¬seen1(cdr y,t)]
∂cTHEN cdr x1(mostrecent(t,λt1.¬seen1(cdr(x1(t1)),t)))
∂b ELSE IF ¬atom x1(t) THEN car x1(t)
∂b ELSE x1(t)]
∂a ELSE x1(t)]

∀t.[x2(t+1) →=_∂aIF pc(t) = 0 THEN x2
∂aELSE IF pc(t) = 1 THEN
→[∂bIF [∃y.seen2(y,t) ∧ ¬atom y ∧ [¬seen2(car y,t) ∨ ¬seen2(cdr y,t)]
∂cTHEN cdr x2(mostrecent(t,λt1.¬seen2(cdr(x2(t1)),t)))
∂bELSE x2(t)]
∂aELSE IF pc(t) = 2 THEN
→[∂bIF [∃y.seen2(y,t) ∧ ¬atom y ∧ [¬seen2(car y,t) ∨ ¬seen2(cdr y,t)]
∂cTHEN cdr x2(mostrecent(t,λt1.¬seen2(cdr(x2(t1)),t)))
∂b ELSE IF ¬atom x2(t) THEN car x2(t)
∂b ELSE x2(t)]
∂a ELSE x2(t)]

∀t.[pc(t+1) →=_∂aIF (pc(t) = 1 ∨ pc(t) = 2 ∧ atom x1(t) ∧ atom x2(t) ∧ x1(t) ≠ x2(t)
∂bTHEN 4
∂aELSE IF pc(t) = 2 ∧ atom x1(t) ∧ atom x2(t) THEN 1
∂aELSE IF ∂bpc(t) = 1
→∧_∂b∀y.[seen1(y,t) ⊃ atom y ∨ seen1(car y,t) ∧ seen1(cdr y,t)]
→∧_∂b∀y.[seen2(y,t) ⊃ atom y ∨ seen2(car y,t) ∧ seen2(cdr y,t)]
∂cTHEN 5
∂aELSE IF ∂bpc(t) = 1
→∧_[∂b∀y.[seen1(y,t) ⊃ atom y ∨ seen1(car y,t) ∧ seen1(cdr y,t)]
→∨_∂b∀y.[seen2(y,t) ⊃ atom y ∨ seen2(car y,t) ∧ seen2(cdr y,t)]]
∂cTHEN 4
∂a ELSE pc(t) + 1]

%1where%2

∀y t.[seen1(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x1(t1)]]

%1and%2

∀y t.[seen2(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x2(t1)]].

.end

	As Thurber might have put it, compared to the recursive definition,
this is a little big and pretty ugly.  However, it does have a certain
brute force straightforward character, and it certainly leaves to the
compiler the task of inventing suitable data structures.

	The theorem to be proved is

%2(samefringe(x1,x2) ≡ ∃t.(pc(t) = 5)) ∧ (¬samefringe(x1,x2) ≡ ∃t.(pc(t) = 4))%1.
.end

#. Parallel processes for computing a sum of functions

.begin
.turn on "[]↑↓&"
.font B "BDJ20"

	The following Elephant program computes %AS%B↑N&↓[n=1]%2f(n))%1
using ⊗k processors.  A master processor with program counter ⊗pc(t) 
initializes the variables ⊗n and ⊗s and starts the ⊗k slave
processes whose program counters are written ⊗pc(i,t) 
at step 1.  A process needs exclusive access to ⊗n when
reading and incrementing it, need exclusive access
to ⊗s when incrementing it, and we only provide for exclusive access
at these times.  We presuppose that computing ⊗f(n) takes ⊗time(n) units
of time, and these operations are done in parallel.  ⊗pc(t) is the
program counter for the master process, and ⊗pc(i,t) is the program
counter of the %2i%1th slave process.  The updating of all variables
except the ⊗pc(i,t) works as in Algolic programs, but the latter
requires a more elaborate and somewhat implicit description that may
well challenge the designer of an Elephant compiler.
.end

.begin nofill
.ww←10
%2 

n(t+1)→=_∂(ww)IF pc(t) = 0 THEN 1
∂(ww)ELSE IF pc(i,t) = 1 ∧ n(t) ≤ N THEN n(t) + 1
∂(ww)ELSE n(t)

s(t+1)→=_∂(ww)IF pc(t) = 0 THEN 0
∂(ww)ELSE IF pc(i,t) = 5 THEN s(t) + m(i,t)
∂(ww)ELSE s(t)

m(i,t+1)→=_∂(ww)IF pc(i,t) = 3 ∧ n(t) ≤ N THEN n(t)
∂(ww)ELSE IF pc(i,t+1) = 4 THEN f(m(i,t))
∂(ww)ELSE m(i,t)

pc(t+1) →=_∂(ww)IF pc(t) = 1 ∧ ∃i.(pc(i,t) ≠ 0) THEN 1
∂(ww)ELSE pc(t) + 1


pc(i,0) = 0

pc(i,t) = 0 ⊃ pc(i,t+1) = IF pc(t) = 0 THEN 1 ELSE 0

pc(i,t) = 1 ⊃ ∃!j.(pc(j,t) = 1 ∧ pc(j,t+1) = 2) ∧ ∃t'.(t < t' ≤ t+k ∧ pc(i,t') = 2)

pc(i,t) = 1 ⊃ pc(i,t+1) = 1 ∨ pc(i,t+1) = 2

pc(i,t) = 2 ⊃ pc(i,t+1) = IF n(t) ≤ N THEN 3 ELSE 0

pc(i,t) = 3 ∧ pc(i,t-1) ≠ 3 
∂(ww)⊃ ∀t'.(t ≤ t' < t + time(m(i,t)) ⊃ pc(i,t') = 3) ∧ pc(t+time(m(i,t))) = 4

pc(i,t) = 4 ⊃ ∃!j.(pc(j,t) = 4 ∧ pc(j,t+1) = 5) ∧ ∃t'.(t < t' ≤ t + k ∧ pc(i,t') = 5)

pc(i,t) = 5 ⊃ pc(i,t+1) = 1
.end

	It may be questioned whether the above Elephant program should be
regarded as a "program" that can be compiled by a suitable compiler or as
something between a specification and a program.  Perhaps it is an example
of that elusive concept called an algorithm.  Notice that it assumes that
synchronization occurs without specifying any way of doing it.  Just the
thing to challenge a smart compiler or automatic programming system.  On
the other hand, the correctness of the Elephant program is given by the
statement,

.begin nofill
.turn on "[]↑↓&"
.font B "BDJ20"

%2∃t.(pc(t) = 2 ∧ ∀i(pc(i,t) = 0) ∧ s(t) = %AS%B↑N&↓[n=1]%2f(n))%1
.end

and this can presumably be proved from the program.  The correspondence
between this Elephant program and one that is more explicit about
synchronization might be proved separately.

	There may well be better ways of describing parallel processes
in Elephant.

#. Equivalence of Elephant programs.

.begin
.turn on "↓"
.at "uu" ⊂"%3u%*"⊃
.at "vv" ⊂"%3v%*"⊃
.at "xx" ⊂"%3x%*"⊃
.at "yy" ⊂"%3y%*"⊃

	Definitions of the equivalence of Elephant programs,
equivalence-preserving transformations of programs, and techniques for
proving equivalence can be expected to be important in applications of
Elephant.  For example, one approach to compiling Elephant is to transform
the program into an immediate program using equivalence-preserving
transformations.

	Equivalence relations should be defined that will facilitate
this process.  An obvious form of equivalence is to require that each
variable in the two programs be represented by the same function of
time for all values of the parameters.  This is too strict an equivalence
to be interesting on two grounds.  First, the two forms of the multiplication
by addition program in section 2 would not be equivalent, because
one of them goes around the loop in one time step while the other takes
four steps.  Second, transforming a program to an immediate program may
involve the introduction of new variables, arrays and other data structures
in order to eliminate the direct references to the past.

	We cannot %2a priori%1 exclude the possibility that several
concepts of equivalence will be useful.  However, our first attempt
is based on the idea that correspondence of times doesn't matter so
long as the correspondence is monotonic and that we are interested only
a certain correspondence between the states of the program.

	Let one Elephant program ⊗P have functions ⊗u↓1(t),_..._,u↓m(t) and
a second ⊗P' have functions ⊗u↓1'(t)_..._u↓n'(t).  In order to avoid prolixity,
we shall summarize these functions as vectors %2uu(t)%1 and %2uu'(t)%1.  Let
%2EP(uu,uu')%1 be a relation.  Let the first depend on
parameters %2x↓1,_..._x↓p%1 and the second have parameters %2x↓1'_..._x↓q'%1,
similarly summarized into vectors %2xx%1 and %2xx'%1.
(The parameters of the program for multiplication by addition were ⊗m and ⊗n). 
Let %2EP(xx,xx')%1 be a relation between the parameters.
Also let %2I(xx)%1 and %2I'(xx')%1 be predicates that say what states of the
two programs are to be compared.
Now suppose we can prove that

	%2P ∧ P' ∧ EP(xx,xx') ⊃ EV(uu(0),uu'(0)) ∧ I(uu(0)) ∧ I'(uu'(0))%1

and

	%2P ∧ P' ⊃ ∀t1 t2 t1'.[EV(uu(t1),uu'(t1')) ∧ t2 >t1 ∧ I(uu(t2))
 ⊃ ∃t2'.EV(uu(t2),uu'(t2'))]%1

and going the other way

	%2P ∧ P' ⊃ ∀t1 t1' t2'.[EV(uu(t1),uu'(t1')) ∧ t2' >t1' ∧ I'(uu'(t2'))
 ⊃ ∃t2.EV(uu(t2),uu'(t2'))]%1.

We should then call the programs ⊗P and ⊗P' equivalent with respect
to the the conditions ⊗I and ⊗I' and the relations ⊗EP and ⊗EV. 
Note that we have used the programs themselves as hypotheses since we can
regard a program as the conjunction of its constituent sentences.

	The two versions of multiplication by addition are equivalent
with respect to the predicates

	%2EP(m,n,m',n') ≡ m=m' ∧ n=n'%1

and

	%2EV(i,p,pc,i',p',pc') ≡ (pc=0 ∧ pc'=0) ∨
[i=i' ∧ p=p' ∧ (pc=2 ∧ pc'=1 ∨ pc=6 ∧ pc'=2)]%1

They should be sufficient to prove that one program is correct (according
to the definitlons of section 2) if and only if the other is.
We expect to give less trivial examples of equivalence and maybe a proof
of equivalence in the final version of this paper.
.end

	Input-output equivalence, i.e. that two programs give the same
output sequence for any sequence of inputs, seems to be a special case of the
above, and there
is reason to hope that it will
suffice for many applications.

#. Remarks

1. Programs in Lucid (Ashcroft and Wadge 1976) are also collections of sentences 
in a first order language.  A Lucid object is a vector of the values 
of a variable throughout time.  This permits some statements to be
made in a very neat way.  However, it seems to be less flexible than
the Elephant device of admitting the time as an explicit parameter.
Lucid programs do not admit qgs, and there are other unexpected
restrictions.  Perhaps some of Lucid's problems would be cured by
including the history of the program counter as a variable.

2. The properties of Elephant programs don't depend on time taking
integer values.  All we need require is that the set of times be ordered
and unbounded above.  Then the first sentence of the product program
would take the form
.begin nofill
.u←20

%2∀t ∃t'.[t' > t ∧ i(t') →=_∂uIF pc(t) = 0 THEN n
∂uELSE IF pc(t) = 3 THEN i(t) - 1
∂uELSE i(t)].
.end

3. It seems to me that any language that purports to allow the user to say
what he wants the computer to do in English, should allow the executive or
general or other big shot to say that %2a customer has a reservation if he
has made one and it hasn't been cancelled%1.  The big shot certainly
doesn't want to concern himself with what data structures are required in
order to fulfill his wishes, and Elephant shows that his wishes can be
stated without mentioning such a data structure.

4. In its present state, Elephant doesn't seem to be a very easy
language to use.  I say "seem", because the awkward programs may
be merely a consequence of inexperience.  Of course, Algolic programs
can easily be translated into Elephant, but this doesn't take
advantage of Elephant's ability to refer directly to the past.

5. Regarded simply as a way of writing Algolic programs as logical
sentences, Elephant plays a role similar to that played by the Cartwright
way of writing Lisp style recursive conditional expression programs as
logical sentences.  In fact it may be a kind of dual to the Cartwright
method just as %2inductive assertions%1 and %2subgoal induction%1 seem to
be duals.  Namely, Elephant programs and inductive assertions work from an
initial state and describe its changes, while Lisp style programs and
subgoal induction work backwards from desired final result.  Thus it may
complete a pattern of methods of program formalization.

6. Elephant may be expanded by relaxing the restriction that statements
refer only to the past.  Our big shot may wish to say, %2"When the
passengers arrive at the airport for the flight, an airplane and a crew
will have been summoned by the scheduling program to fly them to their
destination"%1.  Allowing the right hand sides of Elephant equations to
refer to the future puts a heavier burden on the compiler.  In fact, many
futuristic Elephant program are contradictory and hence uncompilable.
Thus a compiler for futuristic Elephant is really a kind of problem
solver.  Nevertheless, this style of programming may prove practicaly
useful and theoretically illuminating.

8. Church (1957) represents digital circuits as recursive systems of Boolean
equations determining the behavior of a collection of Boolean
variables as a function of time.  He discusses the synthesis of circuits
with given behavior.  Some of his results might lead to theorems
about classes of Elephant programs over finite domains in cases where
the finiteness of the domain is important.
#. References

%3Ashcroft, E. A. and W. W. Wadge (1976)%1: Lucid - A Formal System
for Writing and Proving Programs, %2Siam Journal of Computing%1,
Vol. 5, No. 3, September.

%3Cartwright, R.S. (1976)%1:
%2A Practical Formal Semantic Definition and Verification System
for Typed Lisp%1,
Ph.D. Thesis, Computer Science Department, Stanford University,
Stanford, California.

%3Cartwright, Robert and John McCarthy (1979)%1: "Recursive Programs
as Functions in a First Order Theory", in E. Blum and S. Takasu (eds.),
%2Proceedings of the International
Conference on Mathematical Studies of Information Processing%1, Springer
Publishers.

%3Church, Alonzo (1957)%1: "Application of Recursive Arithmetic to the
Problem of Circuit Synthesis", in %2Summaries of talks presented at the
Summer Institute for Symbolic Logic, Cornell University 1957%1.,
Institute for Defense Analyses.

%3Francez, Nissim and Amir Pnueli (1978)%1: "A Proof Method for Cyclic
Programs", %2Acta Informatica%1 9, 133-157.

%3Francez, Nissim (1976)%1: %2The Analysis of Cyclic Programs%1, PhD
Thesis, Weizmann Institute of Science, Rehovot, Israel.

%3Francez, Nissim (1978)%1: "An Application of a Method for
Analysis of Cyclic Programs", %2IEEE Transactions on Software
Engineering%1, vol. SE-4, No. 5, pp. 371-378, September 1978.

%3Kroger, F. (1978)%1: "A Uniform Logical Basis for the Description,
Specification and Verification of Programs", in E.J. Neuhold (ed.),
%2Formal Descriptions of Programming Concepts%1, North-Holland.

%3McCarthy, John and Carolyn Talcott (1980)%1: 
%2LISP: Programming and Proving%1,
(in preparation)
.if false then begin
Notes

1979 March 30

What concept of equivalence of Elephant programs should be used?

What should be proved about airline program?

Another example where data structure is not specified?
Maybe topological sort?
(General example: do not treat an item that has been previously treated)

Can elephant idea be extended to interacting parallel programs?

1979 March 31

Suppose a function is computed by an elephant program.  How does one
define the function and prove its properties?  Example: append or reverse.

How is a program equivalent to one which is obtained from it by
introducing a new variable and computing it?  We need a concept of
equivalence of programs w/r set of variables.  

Parallel programs

	Consider the following Algolic program in which two processes
co-operate in finding the largest element of an array.

.begin nofill
%2 
∂9n := 1; b := 0;	∂(40)0
∂9qg l1,l2;∂(40)1
l1:∂9if n = N qthen qg done;∂(40)2
∂9b := max(b,a[n]);∂(40)3
∂9n := n + 1;∂(40)4
∂9qgl1;∂(40)5

l2:∂9if n = N qthen qg done;∂(40)2
∂9b := max(b,a[n]);∂(40)3
∂9n := n + 1;∂(40)4
∂9qgl2;∂(40)5

done:∂(40)6
.end

The intent is that the two programs share the variables ⊗b and ⊗n and
merge when they reach ⊗done.  It is also important that they not
interfere with each other.  We can describe this process using
the ideas of Elephant as follows:

It looks like the matching problem provides a conundrum for tense logic
and perhaps there should be a new tense giving the time that matches a
given time.

Inductive assertions

The partial correctness statement is

	%2∀t.(pc(t) = done ∧ ∀t'[0≤t'≤t ⊃ inprog pc(t')] ⊃ p(t) = m*n)%1

We prove by assuming %2pc(t) = done ∧ ∀t'[0≤t'≤t ⊃ inprog pc(t')]%1
and doing induction on

	%2qF(j) ≡ ∀t'[0 ≤ t - t' - 1 ≤ j ∧ pc(t') = start+2 ∧ p(t') = m*(n - i(t'))
⊃ p(t) = m*n]%1.

	qF(0) includes the condition ⊗t_-_t'_1_=_0, i.e. the program
must be just about to jump to ⊗done.  Therefore we must have ⊗i(t')_=_0 or
the program wouldn't jump, i.e. we wouldn't have ⊗pc(t)_=_pc(t'+1)_=_done.  From
this follows ⊗p(t')_=_m*n and consequently ⊗p(t)_=_m*n which was to
be proved.  If ⊗t'_=_t-1, the program, we can follow the program once
around the loop, see that the "invariant" is preserved and reduce the
problem to that for a smaller ⊗j.  Note that the induction is essentially
on time and we do not need to prove that ⊗i(t) decreases.
.end
.SKIP 1
This partial draft of ELEPHA[W80,JMC] compiled at {time} on {date}.